; COMMAND-LINE: -i --sat-solver=cadical
(set-logic QF_BV)
(declare-const x Bool)
(declare-fun p () Bool)
(assert (not (= (_ bv0 4) (ite p (_ bv0 4) (ite x (_ bv1 4) (_ bv0 4))))))
(push)
(set-info :status sat)
(check-sat)
(pop)
(assert (= (_ bv0 3) ((_ extract 2 0) (ite x (_ bv1 4) (_ bv0 4)))))
(push)
(set-info :status unsat)
(check-sat)
(pop)
(set-info :status unsat)
(check-sat)
